\RequirePackage{amsmath,gslist,ulem,proof}
\normalem

\newcommand\sub[1]{[\@sub{#1}]}
\newlist\@sub{\comp}{,\,}{;}{}{^}
\newcommand\comp[1]{\@comp#1\@end}
\newcommand\@comp{}
\def\@comp#1<-#2\@end{#1/#2}

\newcommand\smap[1]{\langle\@smap{#1}\rangle}
\newlist\@smap{\sm}{,\,}{;}{}{^}
\newcommand\sm[1]{\@sm#1\@end}
\newcommand\@sm{}
\def\@sm#1<-#2\@end{#1\mapsto#2}

\newcommand\nt[1]{\mathcal#1}
\newcommand\PP{\nt P}
\newcommand\VV{\nt V}
\newcommand\EE{\nt E}
%\newcommand\NN{\nt N}
\newcommand\UU{\nt U}
\newcommand\BB{\nt B}
\newcommand\FF{\nt F}
%\let\abl\vdash
\let\abl\Rightarrow
\def\abls{\stackrel*\abl}

\renewcommand\SS{\mathcal S} % set of states
\newcommand\CC{\mathcal C} % set of configurations
\let\tr\Rightarrow % transition relation
\def\trs{\stackrel*\tr}
%\newcommand\Nat{{\mathbb{Z}}}
\newcommand\Int{{\mathbb{Z}}}
%\newcommand\kw[1]{\mbox{\sffamily\bfseries#1}}
\newcommand\kw[1]{\mbox{\sffamily#1}}
\newcommand\SKIP{\kw{skip}}
\newcommand\ABORT{\kw{abort}}
\newcommand\REPEAT{\kw{repeat}}
\newcommand\UNTIL{\kw{until}}
\newcommand\WHILE{\kw{while}}
\newcommand\DO{\kw{do}}
\newcommand\OD{\kw{od}}
\newcommand\IF{\kw{if}}
\newcommand\THEN{\kw{then}}\newcommand\ELSE{\kw{else}}
\newcommand\FI{\kw{fi}}
\newcommand\ASS[2]{\mbox{$#1:=#2$}}
\newcommand\ASSERT[1]{\mbox{$\{\,#1\,\}$}}
\newcommand\ASSERTN[2]{\mbox{$\{\,#1\colon #2\,\}$}}
\newcommand\set[1]{\{\,#1\,\}}
\newcommand\Set[2]{\{\,#1\mid#2\,\}}
\newcommand\SET[2]{\{\,#1\mid\text{#2}\,\}}
\let\TAB\quad
\newlength\ALGwidth
%\ALGwidth=\textwidth
%\divide\ALGwidth by 2
\ALGwidth20cm
\newenvironment{ALG}%
   {\begin{minipage}[t]{0cm}
    \begin{tabbing}
    \TAB\=\TAB\=\TAB\=\TAB\=\kill}%
   {\end{tabbing}%
    \end{minipage}%
   }
\newcommand\m[1]{[#1]}
\newcommand\M[1]{\m{#1}\,}
\newcommand\CA[3]{\{\,#1\,\}\,#2\,\{\,#3\,\}}
\let\ua\uparrow
\let\da\downarrow

\newcommand\INV{\mathit{Inv}}
\newcommand\DEF{\mathrm{def}}
\newcommand\FALSE{\mathrm{false}}
\newcommand\TRUE{\mathrm{true}}

\newcommand\WH[2]{\infer[\text{\tiny(wh)}]{#1}{#2}}
\newcommand\WHt[4]{\infer[\text{\tiny(wht)}]{#1}{#2&#3&#4}}
\newcommand\WHta[3]{\infer[\text{\tiny(wht$'$)}]{#1}{#2&#3}}
\newcommand\WHtb[2]{\infer[\text{\tiny(wht$''$)}]{#1}{#2}}
\newcommand\WHtc[2]{\infer[\text{\tiny(wht$'''$)}]{#1}{#2}}
\newcommand\La[4]{\infer[\text{\tiny(lc)}]{#1}{#2&#3&#4}}
\newcommand\Lb[3]{\infer[\text{\tiny(lc)}]{#1}{#2&#3}}
\newcommand\SC[3]{\infer[\text{\tiny(sc)}]{#1}{#2&#3}}
\newcommand\Ia[3]{\infer[\text{\tiny(if)}]{#1}{#2&#3}}
\newcommand\Ib[3]{\infer[\text{\tiny(if$'$)}]{#1}{#2&#3}}
\newcommand\SK[1]{\axiom{\text{\tiny(sk)}}{#1}}
\newcommand\AB[1]{\axiom{\text{\tiny(ab)}}{#1}}
\newcommand\ABt[1]{\axiom{\text{\tiny(abt)}}{#1}}
\newcommand\Aa[1]{\axiom{\text{\tiny(as)}}{#1}}
\newcommand\Ab[1]{\axiom{\text{\tiny(as$'$)}}{#1}}
\newcommand\FRM[2]{\formula{\text{\tiny(#1)}}{#2}}
\newif\ifinfer
\inferfalse
\newcommand\axiom  [2]%
   {\ifinfer\begin{array}[b]{@{}c@{}}#1\\#2\end{array}%
    \else #2\ #1\fi}
\newcommand\formula[2]%
   {\ifinfer\begin{array}[b]{@{}c@{}}#1\\#2\end{array}%
    \else #2\ #1\fi}

\newcommand\EMPH[1]{\boldmath\bfseries#1}
\newcommand\DONE[1]{\sout{#1}}

\let\lfi\Rightarrow

\newcommand\TPL{\textsc{Tpl}}
\newcommand\Sin{\SS_{\mathrm{in}}}
\newcommand\Sout{\SS_{\mathrm{out}}}
\newcommand\Sim[1]{\stackrel{#1}\sim}
\newcommand\defeq{\stackrel{\mathrm{def}}=}
\newcommand\Prime{\mathrm{prime}}
\newcommand\WP{\mathrm{wp}}
\newcommand\WLP{\mathrm{wlp}}
\newcommand\SP{\mathrm{sp}}
\newcommand\PRE{\mathit{Pre}}
\newcommand\POST{\mathit{Post}}
